Propositions as Types

Propositions as Types(型としての命題)

数理論理学での論理は、依存型理論での型と本質的に同じと見なすことができるというやつ

命題(proposition) = 型(type)

$ \mathrm{ proof : Proposition} \cong \mathrm{term : Type}

証明を関数(λ項: 証明項と呼ぶ)、命題を証明項のデータ型とみなす

単純型理論から依存型理論まで進化(?)すると命題を扱えるようになる？

$ \begin{array}{c|c} \mathrm{英語} & \mathrm{型理論} \\ \hline \mathrm{True} & \mathbf{1} \\ \mathrm{False} & \mathbf{0} \\ \text{A and B} & A \times B \\ \text{A or B} & A + B \\ \text{If A then B} & A \rightarrow B \\ \text{A if and only if B} & (A \rightarrow B ) \times (B \rightarrow A) \\ \text{Not A} & A \rightarrow \mathbf{0} \end{array}

ref: 『Homotopy Type Theory: Univalent Foundations of Mathematics』 P42

論理学の記載に変更

$ \begin{array}{c|c} \mathrm{論理} & \mathrm{型理論} \\ \hline \top & \mathbf{1} \\ \bot & \mathbf{0} \\ A \land B & A \times B \\ A \lor B & A + B \\ A \implies B & A \rightarrow B \\ A \iff B & (A \rightarrow B ) \times (B \rightarrow A) \\ \lnot A & A \rightarrow \mathbf{0} \end{array}

$ \mathbf{0} は空型(empty type)

and(A∧B)と$ \times (デカルト積)

証明Aと証明B

$ \frac{x: A \quad y: B }{(x, y) : A \times B}

or(P∨Q)と非交和

$ A + B

If A and Bは関数f : A → Bに対応

A, Bは型

否定(negation)の$ \lnot A は$ A \to \mathbf{0} に対応